\begin{tabbing}
$\forall$\=$A$, $C$:Type, $B$:($A$$\rightarrow$Type), ${\it eqa}$:EqDecider($A$), ${\it eqc}$:EqDecider($C$), $r$:($A$$\rightarrow$$C$), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$),\+
\\[0ex]$a$:$A$.
\-\\[0ex]Inj($A$; $C$; $r$) $\Rightarrow$ $a$ $\in$ dom($f$) $\Rightarrow$ rename($r$;$f$)($r$($a$)) $=$ $f$($a$) $\in$ $B$($a$)
\end{tabbing}